1
2
3
4
5 import java.util.ArrayList;
6 import java.util.Arrays;
7 import java.util.Collection;
8 import java.util.Iterator;
9 import java.util.List;
10
11 import net.sf.javabdd.BDD;
12 import net.sf.javabdd.BDDDomain;
13 import net.sf.javabdd.BDDFactory;
14 import net.sf.javabdd.BDDPairing;
15
16 /***
17 * RubiksCube
18 *
19 * @author jwhaley
20 */
21 public class RubiksCube {
22
23 static BDDFactory bdd;
24 static int n = 3;
25 static int k = 6;
26
27 public static void main(String[] args) {
28 bdd = BDDFactory.init(1000000, 100000);
29 bdd.setMaxIncrease(250000);
30
31 if (args.length > 0) {
32 k = Integer.parseInt(args[0]);
33 }
34
35
36 int[] sizes = new int[n * n * 6];
37
38 Arrays.fill(sizes, 6);
39
40 BDDDomain[] squares = bdd.extDomain(sizes);
41
42 List perms = new ArrayList(12);
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58 int i;
59
60
61 int[] p1 = new int[54];
62 for (i = 0; i < 4 * n; ++i) {
63 int k = (i + n) % (4 * n);
64 p1[i] = k;
65 }
66 for (int j = 0 ; j < 4 * n - 4; ++i, ++j) {
67 int k = 4 * n + ((j + n - 1) % (4 * n - 4));
68 p1[i] = k;
69 }
70 for ( ; i < p1.length; ++i) {
71 int k = i;
72 p1[i] = k;
73 }
74 buildPerm(perms, p1);
75
76
77 int[] p3 = new int[54];
78 for (i = 0; i < 8 * n - 4; ++i) {
79 int k = i;
80 p3[i] = k;
81 }
82 for (int j = 0 ; j < 4 * n; ++i, ++j) {
83 int k = 8 * n - 4 + ((j + n) % (4 * n));
84 p3[i] = k;
85 }
86 for (int j = 0 ; j < 4 * n - 4; ++i, ++j) {
87 int k = 12 * n - 4 + ((j + n - 1) % (4 * n - 4));
88 p3[i] = k;
89 }
90 for ( ; i < p3.length; ++i) {
91 int k = i;
92 p3[i] = k;
93 }
94 buildPerm(perms, p3);
95
96
97 int[] p5 = { 2, 42, 22, 34, 4, 5, 6, 7, 8, 9,
98 10, 14, 3, 43, 23, 15, 16, 17, 18, 19,
99 0, 40, 20, 32, 24, 25, 26, 27, 28, 29,
100 30, 12, 11, 51, 31, 35, 36, 37, 38, 39,
101 1, 41, 21, 33, 44, 45, 46, 47, 48, 49,
102 50, 13, 52, 53 };
103 buildPerm(perms, p5);
104
105
106 int[] p7 = { 0, 1, 16, 5, 45, 25, 36, 7, 8, 9,
107 10, 11, 12, 13, 6, 46, 26, 17, 18, 19,
108 20, 21, 14, 3, 43, 23, 34, 27, 28, 29,
109 30, 31, 32, 33, 2, 42, 22, 37, 38, 39,
110 40, 41, 15, 4, 44, 24, 35, 47, 48, 49,
111 50, 51, 52, 53 };
112 buildPerm(perms, p7);
113
114
115 int[] p9 = { 0, 1, 2, 3, 4, 18, 8, 48, 28, 38,
116 10, 11, 12, 13, 14, 15, 9, 49, 29, 19,
117 20, 21, 22, 23, 24, 16, 6, 46, 26, 36,
118 30, 31, 32, 33, 34, 35, 5, 45, 25, 39,
119 40, 41, 42, 43, 44, 17, 7, 47, 27, 37,
120 50, 51, 52, 53 };
121 buildPerm(perms, p9);
122
123
124 int[] p11= {32, 1, 2, 3, 4, 5, 6, 7, 12, 11,
125 51, 31, 20, 13, 14, 15, 16, 17, 0, 40,
126 38, 21, 22, 23, 24, 25, 26, 27, 18, 9,
127 49, 29, 28, 33, 34, 35, 36, 37, 8, 48,
128 39, 41, 42, 43, 44, 45, 46, 47, 19, 10,
129 50, 30, 52, 53 };
130 buildPerm(perms, p11);
131
132 int[] px = { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
133 10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
134 20, 21, 22, 23, 24, 25, 26, 27, 28, 29,
135 30, 31, 32, 33, 34, 35, 36, 37, 38, 39,
136 40, 41, 42, 43, 44, 45, 46, 47, 48, 49,
137 50, 51, 52, 53 };
138
139 BDD cube = buildInitial();
140 BDD allConfigs = cube.id();
141 addAll(k, perms, allConfigs, cube);
142 System.out.println("Number of distinct configurations after "+k+" moves: "+allConfigs.satCount());
143 }
144
145 static void addAll(int depth, List perms, BDD allConfigs, BDD c) {
146 if (depth <= 0) return;
147 for (Iterator i=perms.iterator(); i.hasNext(); ) {
148 BDDPairing p = (BDDPairing) i.next();
149 BDD c2 = c.replace(p);
150 BDD r = c2.imp(allConfigs);
151 if (!r.isOne()) {
152
153 allConfigs.orWith(c2.id());
154 addAll(depth-1, perms, allConfigs, c2);
155 }
156 r.free();
157 c2.free();
158 }
159 }
160
161 static BDD buildInitial() {
162 BDD b = bdd.universe();
163 for (int k=0; k<4; ++k) {
164 for (int i=0; i<n; ++i) {
165 b.andWith(bdd.getDomain(k*n + i).ithVar(k));
166 b.andWith(bdd.getDomain((8+k)*n - 4 + i).ithVar(k));
167 b.andWith(bdd.getDomain((16+k)*n - 8 + i).ithVar(k));
168 }
169 }
170 for (int i=0; i<8; ++i) {
171 b.andWith(bdd.getDomain(4*n+i).ithVar(4));
172 b.andWith(bdd.getDomain(12*n-4+i).ithVar(5));
173 }
174 b.andWith(bdd.getDomain(n*n*6-2).ithVar(4));
175 b.andWith(bdd.getDomain(n*n*6-1).ithVar(5));
176 return b;
177 }
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192 static void printCube(BDD b) {
193 System.out.println(b.toStringWithDomains());
194 indent(); ps(); p(b, 20); p(b, 21); p(b, 22); newLine();
195 indent(); ps(); p(b, 40); p(b, 41); p(b, 42); newLine();
196 indent(); ps(); p(b, 0); p(b, 1); p(b, 2); newLine();
197 p(b, 31); p(b, 51); p(b, 11); ps(); p(b, 12); p(b, 13); p(b, 14); ps(); p(b, 3); p(b, 43); p(b, 23); newLine();
198 p(b, 30); p(b, 50); p(b, 10); ps(); p(b, 19); p(b, 52); p(b, 15); ps(); p(b, 4); p(b, 44); p(b, 24); newLine();
199 p(b, 29); p(b, 49); p(b, 9); ps(); p(b, 18); p(b, 17); p(b, 16); ps(); p(b, 5); p(b, 45); p(b, 25); newLine();
200 indent(); ps(); p(b, 8); p(b, 7); p(b, 6); newLine();
201 indent(); ps(); p(b, 48); p(b, 47); p(b, 46); newLine();
202 indent(); ps(); p(b, 28); p(b, 27); p(b, 26); newLine();
203 newLine();
204 indent(); ps(); p(b, 32); p(b, 33); p(b, 34); newLine();
205 indent(); ps(); p(b, 39); p(b, 53); p(b, 35); newLine();
206 indent(); ps(); p(b, 38); p(b, 37); p(b, 36); newLine();
207 }
208
209 static void ps() {
210 System.out.print(' ');
211 }
212
213 static void indent() {
214 for (int i = 0; i < n; ++i) {
215 System.out.print(" ");
216 }
217 }
218
219 static void newLine() {
220 System.out.println();
221 }
222
223 static void p(BDD b, int d) {
224 BDDDomain dom = bdd.getDomain(d);
225 int v = b.scanVar(dom).intValue();
226 String s = Integer.toString(v);
227 s = " ".substring(s.length())+s;
228 System.out.print(s);
229 }
230
231 static void checkPerm(int[] perm) {
232 int[] p2 = new int[perm.length];
233 System.arraycopy(perm, 0, p2, 0, p2.length);
234 Arrays.sort(p2);
235 for (int i=0; i<p2.length; ++i) {
236 if (p2[i] != i)
237 throw new InternalError(i+" != "+p2[i]);
238 }
239 }
240
241 static void dumpPerm(int[] perm) {
242 System.out.println("Permutation:");
243 for (int i=0; i<perm.length; ++i) {
244 System.out.println(i+" -> "+perm[i]);
245 }
246 System.out.println();
247 }
248
249 static void buildPerm(Collection perms, int[] perm) {
250
251 checkPerm(perm);
252
253 BDDDomain[] dorig = new BDDDomain[perm.length];
254 for (int i = 0; i < dorig.length; ++i) {
255 dorig[i] = bdd.getDomain(i);
256 }
257 BDDDomain[] dperm = new BDDDomain[perm.length];
258 for (int i=0; i<perm.length; ++i) {
259 dperm[i] = bdd.getDomain(perm[i]);
260 }
261 BDDPairing pair = bdd.makePair();
262 pair.set(dorig, dperm);
263 perms.add(pair);
264 pair = bdd.makePair();
265 pair.set(dperm, dorig);
266 perms.add(pair);
267 }
268
269 }